FDL - Nuprl Lemma : crng_all

Nuprl Lemma : crng_all_properties

r:CRng.
Assoc(|r|;+r)
& Ident(|r|;+r;0)
& Inverse(|r|;+r;0;-r)
& Assoc(|r|;*)
& Comm(|r|;*)
& Ident(|r|;*;1)
& BiLinear(|r|;+r;*)
& IsEqFun(|r|;=

)

Up rings 1

Definitions of Statement CRng

Definitions t T, x:A. B(x), P & Q, CRng

Lemmas crng wf, crng properties, rng all properties

Up	rings 1
Definitions of Statement	CRng
Definitions	t T, x:A. B(x), P & Q, CRng
Lemmas	crng wf, crng properties, rng all properties